(declare-fun a () RoundingMode)
(declare-fun b () (_ FloatingPoint 8 24))
(declare-fun c () (_ FloatingPoint 8 24))
(assert (= b (fp.div a ((_ to_fp 8 24) a 1.0) ((_ to_fp 8 24) a 1.6))))
(assert (distinct a roundNearestTiesToEven))
(assert (not (fp.lt (fp.div a c ((_ to_fp 8 24) a 2.0)) ((_ to_fp 8 24) (_ bv0 32)))))
(check-sat)
(assert (= b (fp.div a ((_ to_fp 8 24) a 1.0) ((_ to_fp 8 24) a 1.6))))
(assert (distinct a roundNearestTiesToEven))
(assert (not (fp.lt (fp.div a c ((_ to_fp 8 24) a 2.0)) ((_ to_fp 8 24) (_ bv0 32)))))
(check-sat)
